WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: #abs(#0()) -> #0() #abs(#neg(x)) -> #pos(x) #abs(#pos(x)) -> #pos(x) #abs(#s(x)) -> #pos(#s(x)) #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0 ,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs,#cklt,#compare,#less,insert,insert#1,insert#2 ,insertD,insertD#1,insertD#2,insertionsort,insertionsort#1,insertionsortD ,insertionsortD#1} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs #abs#(#0()) -> c_1() #abs#(#neg(x)) -> c_2() #abs#(#pos(x)) -> c_3() #abs#(#s(x)) -> c_4() #cklt#(#EQ()) -> c_5() #cklt#(#GT()) -> c_6() #cklt#(#LT()) -> c_7() #compare#(#0(),#0()) -> c_8() #compare#(#0(),#neg(y)) -> c_9() #compare#(#0(),#pos(y)) -> c_10() #compare#(#0(),#s(y)) -> c_11() #compare#(#neg(x),#0()) -> c_12() #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#neg(x),#pos(y)) -> c_14() #compare#(#pos(x),#0()) -> c_15() #compare#(#pos(x),#neg(y)) -> c_16() #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#0()) -> c_18() #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)) insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) insert#1#(nil(),x) -> c_23() insert#2#(#false(),x,y,ys) -> c_24() insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) insertD#1#(nil(),x) -> c_28() insertD#2#(#false(),x,y,ys) -> c_29() insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsort#1#(nil()) -> c_33() insertionsortD#(l) -> c_34(insertionsortD#1#(l)) insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) insertionsortD#1#(nil()) -> c_36() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #abs#(#0()) -> c_1() #abs#(#neg(x)) -> c_2() #abs#(#pos(x)) -> c_3() #abs#(#s(x)) -> c_4() #cklt#(#EQ()) -> c_5() #cklt#(#GT()) -> c_6() #cklt#(#LT()) -> c_7() #compare#(#0(),#0()) -> c_8() #compare#(#0(),#neg(y)) -> c_9() #compare#(#0(),#pos(y)) -> c_10() #compare#(#0(),#s(y)) -> c_11() #compare#(#neg(x),#0()) -> c_12() #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#neg(x),#pos(y)) -> c_14() #compare#(#pos(x),#0()) -> c_15() #compare#(#pos(x),#neg(y)) -> c_16() #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#0()) -> c_18() #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)) insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) insert#1#(nil(),x) -> c_23() insert#2#(#false(),x,y,ys) -> c_24() insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) insertD#1#(nil(),x) -> c_28() insertD#2#(#false(),x,y,ys) -> c_29() insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsort#1#(nil()) -> c_33() insertionsortD#(l) -> c_34(insertionsortD#1#(l)) insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) insertionsortD#1#(nil()) -> c_36() - Weak TRS: #abs(#0()) -> #0() #abs(#neg(x)) -> #pos(x) #abs(#pos(x)) -> #pos(x) #abs(#s(x)) -> #pos(#s(x)) #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/2,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,5,6,7,8,9,10,11,12,14,15,16,18,23,24,28,29,33,36} by application of Pre({1,2,3,4,5,6,7,8,9,10,11,12,14,15,16,18,23,24,28,29,33,36}) = {13,17,19,20,21,22,26,27,31,34}. Here rules are labelled as follows: 1: #abs#(#0()) -> c_1() 2: #abs#(#neg(x)) -> c_2() 3: #abs#(#pos(x)) -> c_3() 4: #abs#(#s(x)) -> c_4() 5: #cklt#(#EQ()) -> c_5() 6: #cklt#(#GT()) -> c_6() 7: #cklt#(#LT()) -> c_7() 8: #compare#(#0(),#0()) -> c_8() 9: #compare#(#0(),#neg(y)) -> c_9() 10: #compare#(#0(),#pos(y)) -> c_10() 11: #compare#(#0(),#s(y)) -> c_11() 12: #compare#(#neg(x),#0()) -> c_12() 13: #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) 14: #compare#(#neg(x),#pos(y)) -> c_14() 15: #compare#(#pos(x),#0()) -> c_15() 16: #compare#(#pos(x),#neg(y)) -> c_16() 17: #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) 18: #compare#(#s(x),#0()) -> c_18() 19: #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) 20: #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)) 21: insert#(x,l) -> c_21(insert#1#(l,x)) 22: insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) 23: insert#1#(nil(),x) -> c_23() 24: insert#2#(#false(),x,y,ys) -> c_24() 25: insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) 26: insertD#(x,l) -> c_26(insertD#1#(l,x)) 27: insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) 28: insertD#1#(nil(),x) -> c_28() 29: insertD#2#(#false(),x,y,ys) -> c_29() 30: insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) 31: insertionsort#(l) -> c_31(insertionsort#1#(l)) 32: insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) 33: insertionsort#1#(nil()) -> c_33() 34: insertionsortD#(l) -> c_34(insertionsortD#1#(l)) 35: insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) 36: insertionsortD#1#(nil()) -> c_36() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)) insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsortD#(l) -> c_34(insertionsortD#1#(l)) insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) - Weak DPs: #abs#(#0()) -> c_1() #abs#(#neg(x)) -> c_2() #abs#(#pos(x)) -> c_3() #abs#(#s(x)) -> c_4() #cklt#(#EQ()) -> c_5() #cklt#(#GT()) -> c_6() #cklt#(#LT()) -> c_7() #compare#(#0(),#0()) -> c_8() #compare#(#0(),#neg(y)) -> c_9() #compare#(#0(),#pos(y)) -> c_10() #compare#(#0(),#s(y)) -> c_11() #compare#(#neg(x),#0()) -> c_12() #compare#(#neg(x),#pos(y)) -> c_14() #compare#(#pos(x),#0()) -> c_15() #compare#(#pos(x),#neg(y)) -> c_16() #compare#(#s(x),#0()) -> c_18() insert#1#(nil(),x) -> c_23() insert#2#(#false(),x,y,ys) -> c_24() insertD#1#(nil(),x) -> c_28() insertD#2#(#false(),x,y,ys) -> c_29() insertionsort#1#(nil()) -> c_33() insertionsortD#1#(nil()) -> c_36() - Weak TRS: #abs(#0()) -> #0() #abs(#neg(x)) -> #pos(x) #abs(#pos(x)) -> #pos(x) #abs(#s(x)) -> #pos(#s(x)) #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/2,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:#compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) -->_1 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3 -->_1 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2 -->_1 #compare#(#s(x),#0()) -> c_18():30 -->_1 #compare#(#pos(x),#neg(y)) -> c_16():29 -->_1 #compare#(#pos(x),#0()) -> c_15():28 -->_1 #compare#(#neg(x),#pos(y)) -> c_14():27 -->_1 #compare#(#neg(x),#0()) -> c_12():26 -->_1 #compare#(#0(),#s(y)) -> c_11():25 -->_1 #compare#(#0(),#pos(y)) -> c_10():24 -->_1 #compare#(#0(),#neg(y)) -> c_9():23 -->_1 #compare#(#0(),#0()) -> c_8():22 -->_1 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1 2:S:#compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) -->_1 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3 -->_1 #compare#(#s(x),#0()) -> c_18():30 -->_1 #compare#(#pos(x),#neg(y)) -> c_16():29 -->_1 #compare#(#pos(x),#0()) -> c_15():28 -->_1 #compare#(#neg(x),#pos(y)) -> c_14():27 -->_1 #compare#(#neg(x),#0()) -> c_12():26 -->_1 #compare#(#0(),#s(y)) -> c_11():25 -->_1 #compare#(#0(),#pos(y)) -> c_10():24 -->_1 #compare#(#0(),#neg(y)) -> c_9():23 -->_1 #compare#(#0(),#0()) -> c_8():22 -->_1 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2 -->_1 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1 3:S:#compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) -->_1 #compare#(#s(x),#0()) -> c_18():30 -->_1 #compare#(#pos(x),#neg(y)) -> c_16():29 -->_1 #compare#(#pos(x),#0()) -> c_15():28 -->_1 #compare#(#neg(x),#pos(y)) -> c_14():27 -->_1 #compare#(#neg(x),#0()) -> c_12():26 -->_1 #compare#(#0(),#s(y)) -> c_11():25 -->_1 #compare#(#0(),#pos(y)) -> c_10():24 -->_1 #compare#(#0(),#neg(y)) -> c_9():23 -->_1 #compare#(#0(),#0()) -> c_8():22 -->_1 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3 -->_1 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2 -->_1 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1 4:S:#less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)) -->_2 #compare#(#s(x),#0()) -> c_18():30 -->_2 #compare#(#pos(x),#neg(y)) -> c_16():29 -->_2 #compare#(#pos(x),#0()) -> c_15():28 -->_2 #compare#(#neg(x),#pos(y)) -> c_14():27 -->_2 #compare#(#neg(x),#0()) -> c_12():26 -->_2 #compare#(#0(),#s(y)) -> c_11():25 -->_2 #compare#(#0(),#pos(y)) -> c_10():24 -->_2 #compare#(#0(),#neg(y)) -> c_9():23 -->_2 #compare#(#0(),#0()) -> c_8():22 -->_1 #cklt#(#LT()) -> c_7():21 -->_1 #cklt#(#GT()) -> c_6():20 -->_1 #cklt#(#EQ()) -> c_5():19 -->_2 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3 -->_2 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2 -->_2 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1 5:S:insert#(x,l) -> c_21(insert#1#(l,x)) -->_1 insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)):6 -->_1 insert#1#(nil(),x) -> c_23():31 6:S:insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) -->_1 insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)):7 -->_1 insert#2#(#false(),x,y,ys) -> c_24():32 -->_2 #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)):4 7:S:insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) -->_1 insert#(x,l) -> c_21(insert#1#(l,x)):5 8:S:insertD#(x,l) -> c_26(insertD#1#(l,x)) -->_1 insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)):9 -->_1 insertD#1#(nil(),x) -> c_28():33 9:S:insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) -->_1 insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)):10 -->_1 insertD#2#(#false(),x,y,ys) -> c_29():34 -->_2 #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)):4 10:S:insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) -->_1 insertD#(x,l) -> c_26(insertD#1#(l,x)):8 11:S:insertionsort#(l) -> c_31(insertionsort#1#(l)) -->_1 insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)):12 -->_1 insertionsort#1#(nil()) -> c_33():35 12:S:insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) -->_2 insertionsort#(l) -> c_31(insertionsort#1#(l)):11 -->_1 insert#(x,l) -> c_21(insert#1#(l,x)):5 13:S:insertionsortD#(l) -> c_34(insertionsortD#1#(l)) -->_1 insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)):14 -->_1 insertionsortD#1#(nil()) -> c_36():36 14:S:insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) -->_2 insertionsortD#(l) -> c_34(insertionsortD#1#(l)):13 -->_1 insertD#(x,l) -> c_26(insertD#1#(l,x)):8 15:W:#abs#(#0()) -> c_1() 16:W:#abs#(#neg(x)) -> c_2() 17:W:#abs#(#pos(x)) -> c_3() 18:W:#abs#(#s(x)) -> c_4() 19:W:#cklt#(#EQ()) -> c_5() 20:W:#cklt#(#GT()) -> c_6() 21:W:#cklt#(#LT()) -> c_7() 22:W:#compare#(#0(),#0()) -> c_8() 23:W:#compare#(#0(),#neg(y)) -> c_9() 24:W:#compare#(#0(),#pos(y)) -> c_10() 25:W:#compare#(#0(),#s(y)) -> c_11() 26:W:#compare#(#neg(x),#0()) -> c_12() 27:W:#compare#(#neg(x),#pos(y)) -> c_14() 28:W:#compare#(#pos(x),#0()) -> c_15() 29:W:#compare#(#pos(x),#neg(y)) -> c_16() 30:W:#compare#(#s(x),#0()) -> c_18() 31:W:insert#1#(nil(),x) -> c_23() 32:W:insert#2#(#false(),x,y,ys) -> c_24() 33:W:insertD#1#(nil(),x) -> c_28() 34:W:insertD#2#(#false(),x,y,ys) -> c_29() 35:W:insertionsort#1#(nil()) -> c_33() 36:W:insertionsortD#1#(nil()) -> c_36() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 18: #abs#(#s(x)) -> c_4() 17: #abs#(#pos(x)) -> c_3() 16: #abs#(#neg(x)) -> c_2() 15: #abs#(#0()) -> c_1() 36: insertionsortD#1#(nil()) -> c_36() 35: insertionsort#1#(nil()) -> c_33() 33: insertD#1#(nil(),x) -> c_28() 34: insertD#2#(#false(),x,y,ys) -> c_29() 31: insert#1#(nil(),x) -> c_23() 32: insert#2#(#false(),x,y,ys) -> c_24() 19: #cklt#(#EQ()) -> c_5() 20: #cklt#(#GT()) -> c_6() 21: #cklt#(#LT()) -> c_7() 22: #compare#(#0(),#0()) -> c_8() 23: #compare#(#0(),#neg(y)) -> c_9() 24: #compare#(#0(),#pos(y)) -> c_10() 25: #compare#(#0(),#s(y)) -> c_11() 26: #compare#(#neg(x),#0()) -> c_12() 27: #compare#(#neg(x),#pos(y)) -> c_14() 28: #compare#(#pos(x),#0()) -> c_15() 29: #compare#(#pos(x),#neg(y)) -> c_16() 30: #compare#(#s(x),#0()) -> c_18() * Step 4: SimplifyRHS WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)) insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsortD#(l) -> c_34(insertionsortD#1#(l)) insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) - Weak TRS: #abs(#0()) -> #0() #abs(#neg(x)) -> #pos(x) #abs(#pos(x)) -> #pos(x) #abs(#s(x)) -> #pos(#s(x)) #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/2,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:#compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) -->_1 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3 -->_1 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2 -->_1 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1 2:S:#compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) -->_1 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3 -->_1 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2 -->_1 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1 3:S:#compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) -->_1 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3 -->_1 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2 -->_1 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1 4:S:#less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)) -->_2 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3 -->_2 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2 -->_2 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1 5:S:insert#(x,l) -> c_21(insert#1#(l,x)) -->_1 insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)):6 6:S:insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) -->_1 insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)):7 -->_2 #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)):4 7:S:insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) -->_1 insert#(x,l) -> c_21(insert#1#(l,x)):5 8:S:insertD#(x,l) -> c_26(insertD#1#(l,x)) -->_1 insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)):9 9:S:insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) -->_1 insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)):10 -->_2 #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)):4 10:S:insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) -->_1 insertD#(x,l) -> c_26(insertD#1#(l,x)):8 11:S:insertionsort#(l) -> c_31(insertionsort#1#(l)) -->_1 insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)):12 12:S:insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) -->_2 insertionsort#(l) -> c_31(insertionsort#1#(l)):11 -->_1 insert#(x,l) -> c_21(insert#1#(l,x)):5 13:S:insertionsortD#(l) -> c_34(insertionsortD#1#(l)) -->_1 insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)):14 14:S:insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) -->_2 insertionsortD#(l) -> c_34(insertionsortD#1#(l)):13 -->_1 insertD#(x,l) -> c_26(insertD#1#(l,x)):8 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: #less#(x,y) -> c_20(#compare#(x,y)) * Step 5: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) #less#(x,y) -> c_20(#compare#(x,y)) insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsortD#(l) -> c_34(insertionsortD#1#(l)) insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) - Weak TRS: #abs(#0()) -> #0() #abs(#neg(x)) -> #pos(x) #abs(#pos(x)) -> #pos(x) #abs(#s(x)) -> #pos(#s(x)) #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) #less#(x,y) -> c_20(#compare#(x,y)) insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsortD#(l) -> c_34(insertionsortD#1#(l)) insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) * Step 6: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) #less#(x,y) -> c_20(#compare#(x,y)) insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsortD#(l) -> c_34(insertionsortD#1#(l)) insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsortD#(l) -> c_34(insertionsortD#1#(l)) insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) and a lower component #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) #less#(x,y) -> c_20(#compare#(x,y)) insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) Further, following extension rules are added to the lower component. insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) ** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsortD#(l) -> c_34(insertionsortD#1#(l)) insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:insertionsort#(l) -> c_31(insertionsort#1#(l)) -->_1 insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)):2 2:S:insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)) -->_2 insertionsort#(l) -> c_31(insertionsort#1#(l)):1 3:S:insertionsortD#(l) -> c_34(insertionsortD#1#(l)) -->_1 insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)):4 4:S:insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)) -->_2 insertionsortD#(l) -> c_34(insertionsortD#1#(l)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs)) insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs)) ** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs)) insertionsortD#(l) -> c_34(insertionsortD#1#(l)) insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/1,c_33/0,c_34/1,c_35/1,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs)) insertionsortD#(l) -> c_34(insertionsortD#1#(l)) insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs)) ** Step 6.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs)) insertionsortD#(l) -> c_34(insertionsortD#1#(l)) insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs)) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/1,c_33/0,c_34/1,c_35/1,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- dd :: ["A"(0) x "A"(13)] -(13)-> "A"(13) dd :: ["A"(0) x "A"(15)] -(15)-> "A"(15) insertionsort# :: ["A"(13)] -(10)-> "A"(0) insertionsort#1# :: ["A"(13)] -(0)-> "A"(14) insertionsortD# :: ["A"(15)] -(15)-> "A"(5) insertionsortD#1# :: ["A"(15)] -(0)-> "A"(2) c_31 :: ["A"(0)] -(0)-> "A"(2) c_32 :: ["A"(0)] -(0)-> "A"(14) c_34 :: ["A"(0)] -(0)-> "A"(10) c_35 :: ["A"(0)] -(0)-> "A"(12) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "c_31_A" :: ["A"(0)] -(0)-> "A"(1) "c_32_A" :: ["A"(0)] -(0)-> "A"(1) "c_34_A" :: ["A"(0)] -(0)-> "A"(1) "c_35_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs)) insertionsortD#(l) -> c_34(insertionsortD#1#(l)) 2. Weak: insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs)) ** Step 6.a:4: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs)) - Weak DPs: insertionsort#(l) -> c_31(insertionsort#1#(l)) insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs)) insertionsortD#(l) -> c_34(insertionsortD#1#(l)) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/1,c_33/0,c_34/1,c_35/1,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- dd :: ["A"(0) x "A"(1)] -(1)-> "A"(1) insertionsort# :: ["A"(1)] -(13)-> "A"(8) insertionsort#1# :: ["A"(1)] -(13)-> "A"(14) insertionsortD# :: ["A"(1)] -(15)-> "A"(14) insertionsortD#1# :: ["A"(1)] -(15)-> "A"(0) c_31 :: ["A"(0)] -(0)-> "A"(14) c_32 :: ["A"(0)] -(0)-> "A"(14) c_34 :: ["A"(0)] -(0)-> "A"(14) c_35 :: ["A"(0)] -(0)-> "A"(14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "c_31_A" :: ["A"(0)] -(0)-> "A"(1) "c_32_A" :: ["A"(0)] -(0)-> "A"(1) "c_34_A" :: ["A"(0)] -(0)-> "A"(1) "c_35_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs)) 2. Weak: ** Step 6.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) #less#(x,y) -> c_20(#compare#(x,y)) insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) - Weak DPs: insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) and a lower component #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) #less#(x,y) -> c_20(#compare#(x,y)) Further, following extension rules are added to the lower component. insert#(x,l) -> insert#1#(l,x) insert#1#(dd(y,ys),x) -> #less#(y,x) insert#1#(dd(y,ys),x) -> insert#2#(#less(y,x),x,y,ys) insert#2#(#true(),x,y,ys) -> insert#(x,ys) insertD#(x,l) -> insertD#1#(l,x) insertD#1#(dd(y,ys),x) -> #less#(y,x) insertD#1#(dd(y,ys),x) -> insertD#2#(#less(y,x),x,y,ys) insertD#2#(#true(),x,y,ys) -> insertD#(x,ys) insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) *** Step 6.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) - Weak DPs: insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:insert#(x,l) -> c_21(insert#1#(l,x)) -->_1 insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)):2 2:S:insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)) -->_1 insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)):3 3:S:insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) -->_1 insert#(x,l) -> c_21(insert#1#(l,x)):1 4:S:insertD#(x,l) -> c_26(insertD#1#(l,x)) -->_1 insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)):5 5:S:insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)) -->_1 insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)):6 6:S:insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) -->_1 insertD#(x,l) -> c_26(insertD#1#(l,x)):4 7:W:insertionsort#(l) -> insertionsort#1#(l) -->_1 insertionsort#1#(dd(x,xs)) -> insertionsort#(xs):9 -->_1 insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)):8 8:W:insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) -->_1 insert#(x,l) -> c_21(insert#1#(l,x)):1 9:W:insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) -->_1 insertionsort#(l) -> insertionsort#1#(l):7 10:W:insertionsortD#(l) -> insertionsortD#1#(l) -->_1 insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs):12 -->_1 insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)):11 11:W:insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) -->_1 insertD#(x,l) -> c_26(insertD#1#(l,x)):4 12:W:insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) -->_1 insertionsortD#(l) -> insertionsortD#1#(l):10 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys)) *** Step 6.b:1.a:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) - Weak DPs: insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/1,c_27/1,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(15) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(15) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(15) #cklt :: ["A"(0)] -(0)-> "A"(13) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(9) #false :: [] -(0)-> "A"(1) #false :: [] -(0)-> "A"(0) #false :: [] -(0)-> "A"(15) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(12) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(0) #true :: [] -(0)-> "A"(1) #true :: [] -(0)-> "A"(15) dd :: ["A"(4) x "A"(4)] -(4)-> "A"(4) dd :: ["A"(7) x "A"(7)] -(7)-> "A"(7) dd :: ["A"(8) x "A"(8)] -(8)-> "A"(8) dd :: ["A"(10) x "A"(10)] -(10)-> "A"(10) dd :: ["A"(15) x "A"(15)] -(15)-> "A"(15) dd :: ["A"(11) x "A"(11)] -(11)-> "A"(11) insert :: ["A"(4) x "A"(4)] -(4)-> "A"(4) insert#1 :: ["A"(4) x "A"(4)] -(4)-> "A"(4) insert#2 :: ["A"(1) x "A"(4) x "A"(4) x "A"(4)] -(8)-> "A"(4) insertD :: ["A"(9) x "A"(7)] -(8)-> "A"(7) insertD#1 :: ["A"(7) x "A"(9)] -(8)-> "A"(7) insertD#2 :: ["A"(0) x "A"(9) x "A"(7) x "A"(7)] -(15)-> "A"(7) insertionsort :: ["A"(8)] -(0)-> "A"(4) insertionsort#1 :: ["A"(8)] -(0)-> "A"(4) insertionsortD :: ["A"(10)] -(2)-> "A"(7) insertionsortD#1 :: ["A"(10)] -(2)-> "A"(7) nil :: [] -(0)-> "A"(4) nil :: [] -(0)-> "A"(7) nil :: [] -(0)-> "A"(8) nil :: [] -(0)-> "A"(10) nil :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(11) nil :: [] -(0)-> "A"(13) insert# :: ["A"(0) x "A"(4)] -(0)-> "A"(2) insert#1# :: ["A"(4) x "A"(0)] -(0)-> "A"(9) insert#2# :: ["A"(0) x "A"(0) x "A"(1) x "A"(4)] -(1)-> "A"(13) insertD# :: ["A"(0) x "A"(7)] -(1)-> "A"(4) insertD#1# :: ["A"(7) x "A"(0)] -(1)-> "A"(4) insertD#2# :: ["A"(0) x "A"(0) x "A"(0) x "A"(7)] -(8)-> "A"(13) insertionsort# :: ["A"(15)] -(9)-> "A"(1) insertionsort#1# :: ["A"(15)] -(8)-> "A"(1) insertionsortD# :: ["A"(11)] -(13)-> "A"(4) insertionsortD#1# :: ["A"(11)] -(8)-> "A"(4) c_21 :: ["A"(0)] -(0)-> "A"(5) c_22 :: ["A"(9)] -(0)-> "A"(9) c_25 :: ["A"(0)] -(0)-> "A"(15) c_26 :: ["A"(0)] -(0)-> "A"(8) c_27 :: ["A"(8)] -(0)-> "A"(8) c_30 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(1)] -(1)-> "A"(1) "#pos_A" :: ["A"(1)] -(1)-> "A"(1) "#s_A" :: ["A"(0)] -(1)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_21_A" :: ["A"(0)] -(0)-> "A"(1) "c_22_A" :: ["A"(0)] -(0)-> "A"(1) "c_25_A" :: ["A"(0)] -(0)-> "A"(1) "c_26_A" :: ["A"(0)] -(0)-> "A"(1) "c_27_A" :: ["A"(0)] -(0)-> "A"(1) "c_30_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) 2. Weak: insert#(x,l) -> c_21(insert#1#(l,x)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) *** Step 6.b:1.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insert#(x,l) -> c_21(insert#1#(l,x)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) - Weak DPs: insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/1,c_27/1,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(15) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(15) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(15) #cklt :: ["A"(0)] -(0)-> "A"(13) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(9) #false :: [] -(0)-> "A"(1) #false :: [] -(0)-> "A"(15) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(12) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(0) #true :: [] -(0)-> "A"(1) #true :: [] -(0)-> "A"(15) dd :: ["A"(1) x "A"(1)] -(1)-> "A"(1) dd :: ["A"(5) x "A"(5)] -(5)-> "A"(5) dd :: ["A"(12) x "A"(12)] -(12)-> "A"(12) dd :: ["A"(13) x "A"(13)] -(13)-> "A"(13) dd :: ["A"(15) x "A"(15)] -(15)-> "A"(15) insert :: ["A"(9) x "A"(5)] -(8)-> "A"(5) insert#1 :: ["A"(5) x "A"(9)] -(8)-> "A"(5) insert#2 :: ["A"(1) x "A"(9) x "A"(5) x "A"(5)] -(13)-> "A"(5) insertD :: ["A"(10) x "A"(1)] -(4)-> "A"(1) insertD#1 :: ["A"(1) x "A"(10)] -(4)-> "A"(1) insertD#2 :: ["A"(1) x "A"(10) x "A"(1) x "A"(1)] -(5)-> "A"(1) insertionsort :: ["A"(12)] -(4)-> "A"(5) insertionsort#1 :: ["A"(12)] -(2)-> "A"(5) insertionsortD :: ["A"(13)] -(8)-> "A"(1) insertionsortD#1 :: ["A"(13)] -(5)-> "A"(1) nil :: [] -(0)-> "A"(5) nil :: [] -(0)-> "A"(1) nil :: [] -(0)-> "A"(12) nil :: [] -(0)-> "A"(13) nil :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(11) nil :: [] -(0)-> "A"(7) insert# :: ["A"(1) x "A"(5)] -(3)-> "A"(8) insert#1# :: ["A"(5) x "A"(1)] -(0)-> "A"(12) insert#2# :: ["A"(0) x "A"(1) x "A"(0) x "A"(5)] -(3)-> "A"(13) insertD# :: ["A"(9) x "A"(1)] -(0)-> "A"(0) insertD#1# :: ["A"(1) x "A"(9)] -(0)-> "A"(12) insertD#2# :: ["A"(0) x "A"(9) x "A"(0) x "A"(1)] -(1)-> "A"(13) insertionsort# :: ["A"(15)] -(9)-> "A"(0) insertionsort#1# :: ["A"(15)] -(4)-> "A"(0) insertionsortD# :: ["A"(13)] -(9)-> "A"(0) insertionsortD#1# :: ["A"(13)] -(1)-> "A"(0) c_21 :: ["A"(9)] -(0)-> "A"(9) c_22 :: ["A"(0)] -(0)-> "A"(15) c_25 :: ["A"(0)] -(0)-> "A"(15) c_26 :: ["A"(0)] -(0)-> "A"(12) c_27 :: ["A"(0)] -(0)-> "A"(15) c_30 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(1)] -(0)-> "A"(1) "#pos_A" :: ["A"(1)] -(0)-> "A"(1) "#s_A" :: ["A"(1)] -(0)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_21_A" :: ["A"(0)] -(0)-> "A"(1) "c_22_A" :: ["A"(0)] -(0)-> "A"(1) "c_25_A" :: ["A"(0)] -(0)-> "A"(1) "c_26_A" :: ["A"(0)] -(0)-> "A"(1) "c_27_A" :: ["A"(0)] -(0)-> "A"(1) "c_30_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) 2. Weak: insert#(x,l) -> c_21(insert#1#(l,x)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys)) *** Step 6.b:1.a:4: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insert#(x,l) -> c_21(insert#1#(l,x)) insertD#(x,l) -> c_26(insertD#1#(l,x)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys)) - Weak DPs: insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/1,c_27/1,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(15) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(15) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(15) #cklt :: ["A"(0)] -(0)-> "A"(13) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(9) #false :: [] -(0)-> "A"(1) #false :: [] -(0)-> "A"(15) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(12) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(1) #true :: [] -(0)-> "A"(0) #true :: [] -(0)-> "A"(15) dd :: ["A"(0) x "A"(4)] -(4)-> "A"(4) dd :: ["A"(0) x "A"(7)] -(7)-> "A"(7) dd :: ["A"(0) x "A"(5)] -(5)-> "A"(5) dd :: ["A"(0) x "A"(10)] -(10)-> "A"(10) dd :: ["A"(0) x "A"(11)] -(11)-> "A"(11) dd :: ["A"(0) x "A"(14)] -(14)-> "A"(14) dd :: ["A"(0) x "A"(15)] -(15)-> "A"(15) dd :: ["A"(0) x "A"(8)] -(8)-> "A"(8) insert :: ["A"(0) x "A"(7)] -(8)-> "A"(7) insert#1 :: ["A"(7) x "A"(0)] -(8)-> "A"(7) insert#2 :: ["A"(1) x "A"(0) x "A"(0) x "A"(7)] -(15)-> "A"(7) insertD :: ["A"(0) x "A"(5)] -(9)-> "A"(5) insertD#1 :: ["A"(5) x "A"(0)] -(9)-> "A"(5) insertD#2 :: ["A"(1) x "A"(0) x "A"(0) x "A"(5)] -(14)-> "A"(5) insertionsort :: ["A"(10)] -(1)-> "A"(7) insertionsort#1 :: ["A"(10)] -(1)-> "A"(7) insertionsortD :: ["A"(11)] -(1)-> "A"(5) insertionsortD#1 :: ["A"(11)] -(1)-> "A"(5) nil :: [] -(0)-> "A"(7) nil :: [] -(0)-> "A"(5) nil :: [] -(0)-> "A"(10) nil :: [] -(0)-> "A"(11) nil :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(13) insert# :: ["A"(0) x "A"(7)] -(5)-> "A"(4) insert#1# :: ["A"(7) x "A"(0)] -(0)-> "A"(13) insert#2# :: ["A"(0) x "A"(0) x "A"(0) x "A"(7)] -(5)-> "A"(15) insertD# :: ["A"(0) x "A"(4)] -(0)-> "A"(8) insertD#1# :: ["A"(4) x "A"(0)] -(0)-> "A"(12) insertD#2# :: ["A"(0) x "A"(0) x "A"(0) x "A"(4)] -(2)-> "A"(13) insertionsort# :: ["A"(14)] -(9)-> "A"(4) insertionsort#1# :: ["A"(14)] -(9)-> "A"(4) insertionsortD# :: ["A"(15)] -(9)-> "A"(3) insertionsortD#1# :: ["A"(15)] -(0)-> "A"(3) c_21 :: ["A"(13)] -(0)-> "A"(13) c_22 :: ["A"(13)] -(0)-> "A"(13) c_25 :: ["A"(0)] -(0)-> "A"(15) c_26 :: ["A"(0)] -(0)-> "A"(12) c_27 :: ["A"(0)] -(0)-> "A"(15) c_30 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(0)] -(0)-> "A"(1) "#pos_A" :: ["A"(0)] -(1)-> "A"(1) "#s_A" :: ["A"(1)] -(1)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_21_A" :: ["A"(0)] -(0)-> "A"(1) "c_22_A" :: ["A"(0)] -(0)-> "A"(1) "c_25_A" :: ["A"(0)] -(0)-> "A"(1) "c_26_A" :: ["A"(0)] -(0)-> "A"(1) "c_27_A" :: ["A"(0)] -(0)-> "A"(1) "c_30_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys)) 2. Weak: insert#(x,l) -> c_21(insert#1#(l,x)) insertD#(x,l) -> c_26(insertD#1#(l,x)) *** Step 6.b:1.a:5: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insert#(x,l) -> c_21(insert#1#(l,x)) insertD#(x,l) -> c_26(insertD#1#(l,x)) - Weak DPs: insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/1,c_27/1,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(15) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(15) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(15) #cklt :: ["A"(0)] -(0)-> "A"(13) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(9) #false :: [] -(0)-> "A"(1) #false :: [] -(0)-> "A"(15) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(12) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(1) #true :: [] -(0)-> "A"(0) #true :: [] -(0)-> "A"(15) dd :: ["A"(0) x "A"(6)] -(6)-> "A"(6) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) dd :: ["A"(0) x "A"(13)] -(13)-> "A"(13) dd :: ["A"(0) x "A"(12)] -(12)-> "A"(12) dd :: ["A"(0) x "A"(5)] -(5)-> "A"(5) dd :: ["A"(0) x "A"(14)] -(14)-> "A"(14) dd :: ["A"(0) x "A"(8)] -(8)-> "A"(8) insert :: ["A"(0) x "A"(6)] -(8)-> "A"(6) insert#1 :: ["A"(6) x "A"(0)] -(8)-> "A"(6) insert#2 :: ["A"(1) x "A"(0) x "A"(0) x "A"(6)] -(14)-> "A"(6) insertD :: ["A"(0) x "A"(0)] -(12)-> "A"(0) insertD#1 :: ["A"(0) x "A"(0)] -(12)-> "A"(0) insertD#2 :: ["A"(1) x "A"(0) x "A"(0) x "A"(0)] -(12)-> "A"(0) insertionsort :: ["A"(13)] -(10)-> "A"(6) insertionsort#1 :: ["A"(13)] -(9)-> "A"(6) insertionsortD :: ["A"(12)] -(0)-> "A"(0) insertionsortD#1 :: ["A"(12)] -(0)-> "A"(0) nil :: [] -(0)-> "A"(6) nil :: [] -(0)-> "A"(0) nil :: [] -(0)-> "A"(13) nil :: [] -(0)-> "A"(12) nil :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(7) insert# :: ["A"(0) x "A"(5)] -(2)-> "A"(0) insert#1# :: ["A"(5) x "A"(0)] -(1)-> "A"(13) insert#2# :: ["A"(0) x "A"(0) x "A"(0) x "A"(5)] -(3)-> "A"(13) insertD# :: ["A"(0) x "A"(0)] -(2)-> "A"(8) insertD#1# :: ["A"(0) x "A"(0)] -(2)-> "A"(15) insertD#2# :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(2)-> "A"(13) insertionsort# :: ["A"(14)] -(9)-> "A"(0) insertionsort#1# :: ["A"(14)] -(1)-> "A"(0) insertionsortD# :: ["A"(12)] -(8)-> "A"(4) insertionsortD#1# :: ["A"(12)] -(8)-> "A"(4) c_21 :: ["A"(12)] -(0)-> "A"(12) c_22 :: ["A"(13)] -(0)-> "A"(13) c_25 :: ["A"(0)] -(0)-> "A"(15) c_26 :: ["A"(11)] -(0)-> "A"(11) c_27 :: ["A"(0)] -(0)-> "A"(15) c_30 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(0)] -(1)-> "A"(1) "#pos_A" :: ["A"(0)] -(0)-> "A"(1) "#s_A" :: ["A"(0)] -(1)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_21_A" :: ["A"(0)] -(0)-> "A"(1) "c_22_A" :: ["A"(0)] -(0)-> "A"(1) "c_25_A" :: ["A"(0)] -(0)-> "A"(1) "c_26_A" :: ["A"(0)] -(0)-> "A"(1) "c_27_A" :: ["A"(0)] -(0)-> "A"(1) "c_30_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insert#(x,l) -> c_21(insert#1#(l,x)) 2. Weak: insertD#(x,l) -> c_26(insertD#1#(l,x)) *** Step 6.b:1.a:6: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insertD#(x,l) -> c_26(insertD#1#(l,x)) - Weak DPs: insert#(x,l) -> c_21(insert#1#(l,x)) insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys)) insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)) insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys)) insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)) insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/1,c_27/1,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(14) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(14) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(10) #LT :: [] -(0)-> "A"(6) #LT :: [] -(0)-> "A"(14) #cklt :: ["A"(0)] -(0)-> "A"(0) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #false :: [] -(0)-> "A"(0) #false :: [] -(0)-> "A"(14) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(0) #true :: [] -(0)-> "A"(14) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) dd :: ["A"(0) x "A"(1)] -(1)-> "A"(1) dd :: ["A"(0) x "A"(14)] -(14)-> "A"(14) dd :: ["A"(0) x "A"(9)] -(9)-> "A"(9) dd :: ["A"(0) x "A"(8)] -(8)-> "A"(8) insert :: ["A"(0) x "A"(0)] -(0)-> "A"(0) insert#1 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) insert#2 :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) insertD :: ["A"(0) x "A"(1)] -(12)-> "A"(1) insertD#1 :: ["A"(1) x "A"(0)] -(12)-> "A"(1) insertD#2 :: ["A"(0) x "A"(0) x "A"(0) x "A"(1)] -(13)-> "A"(1) insertionsort :: ["A"(0)] -(1)-> "A"(0) insertionsort#1 :: ["A"(0)] -(1)-> "A"(0) insertionsortD :: ["A"(14)] -(0)-> "A"(1) insertionsortD#1 :: ["A"(14)] -(0)-> "A"(1) nil :: [] -(0)-> "A"(0) nil :: [] -(0)-> "A"(1) nil :: [] -(0)-> "A"(14) nil :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(7) insert# :: ["A"(0) x "A"(0)] -(0)-> "A"(0) insert#1# :: ["A"(0) x "A"(0)] -(0)-> "A"(0) insert#2# :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(12) insertD# :: ["A"(0) x "A"(1)] -(3)-> "A"(6) insertD#1# :: ["A"(1) x "A"(0)] -(2)-> "A"(14) insertD#2# :: ["A"(0) x "A"(0) x "A"(0) x "A"(1)] -(3)-> "A"(2) insertionsort# :: ["A"(9)] -(15)-> "A"(0) insertionsort#1# :: ["A"(9)] -(15)-> "A"(0) insertionsortD# :: ["A"(14)] -(14)-> "A"(6) insertionsortD#1# :: ["A"(14)] -(8)-> "A"(6) c_21 :: ["A"(0)] -(0)-> "A"(14) c_22 :: ["A"(0)] -(0)-> "A"(0) c_25 :: ["A"(0)] -(0)-> "A"(12) c_26 :: ["A"(0)] -(0)-> "A"(14) c_27 :: ["A"(0)] -(0)-> "A"(14) c_30 :: ["A"(0)] -(0)-> "A"(10) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(0)] -(0)-> "A"(1) "#pos_A" :: ["A"(0)] -(0)-> "A"(1) "#s_A" :: ["A"(0)] -(0)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_21_A" :: ["A"(0)] -(0)-> "A"(1) "c_22_A" :: ["A"(0)] -(0)-> "A"(1) "c_25_A" :: ["A"(0)] -(0)-> "A"(1) "c_26_A" :: ["A"(0)] -(0)-> "A"(1) "c_27_A" :: ["A"(0)] -(0)-> "A"(1) "c_30_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insertD#(x,l) -> c_26(insertD#1#(l,x)) 2. Weak: *** Step 6.b:1.b:1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) #less#(x,y) -> c_20(#compare#(x,y)) - Weak DPs: insert#(x,l) -> insert#1#(l,x) insert#1#(dd(y,ys),x) -> #less#(y,x) insert#1#(dd(y,ys),x) -> insert#2#(#less(y,x),x,y,ys) insert#2#(#true(),x,y,ys) -> insert#(x,ys) insertD#(x,l) -> insertD#1#(l,x) insertD#1#(dd(y,ys),x) -> #less#(y,x) insertD#1#(dd(y,ys),x) -> insertD#2#(#less(y,x),x,y,ys) insertD#2#(#true(),x,y,ys) -> insertD#(x,ys) insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(0) #cklt :: ["A"(0)] -(0)-> "A"(0) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #false :: [] -(0)-> "A"(0) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(0) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) insert :: ["A"(0) x "A"(0)] -(0)-> "A"(0) insert#1 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) insert#2 :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) insertD :: ["A"(0) x "A"(0)] -(0)-> "A"(0) insertD#1 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) insertD#2 :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) insertionsort :: ["A"(0)] -(0)-> "A"(0) insertionsort#1 :: ["A"(0)] -(0)-> "A"(0) insertionsortD :: ["A"(0)] -(0)-> "A"(0) insertionsortD#1 :: ["A"(0)] -(0)-> "A"(0) nil :: [] -(0)-> "A"(0) #compare# :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #less# :: ["A"(0) x "A"(0)] -(1)-> "A"(0) insert# :: ["A"(0) x "A"(0)] -(1)-> "A"(0) insert#1# :: ["A"(0) x "A"(0)] -(1)-> "A"(0) insert#2# :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(1)-> "A"(0) insertD# :: ["A"(0) x "A"(0)] -(1)-> "A"(0) insertD#1# :: ["A"(0) x "A"(0)] -(1)-> "A"(0) insertD#2# :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(1)-> "A"(0) insertionsort# :: ["A"(0)] -(1)-> "A"(0) insertionsort#1# :: ["A"(0)] -(1)-> "A"(0) insertionsortD# :: ["A"(0)] -(1)-> "A"(0) insertionsortD#1# :: ["A"(0)] -(1)-> "A"(0) c_13 :: ["A"(0)] -(0)-> "A"(0) c_17 :: ["A"(0)] -(0)-> "A"(0) c_19 :: ["A"(0)] -(0)-> "A"(0) c_20 :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: #less#(x,y) -> c_20(#compare#(x,y)) 2. Weak: #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) *** Step 6.b:1.b:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) - Weak DPs: #less#(x,y) -> c_20(#compare#(x,y)) insert#(x,l) -> insert#1#(l,x) insert#1#(dd(y,ys),x) -> #less#(y,x) insert#1#(dd(y,ys),x) -> insert#2#(#less(y,x),x,y,ys) insert#2#(#true(),x,y,ys) -> insert#(x,ys) insertD#(x,l) -> insertD#1#(l,x) insertD#1#(dd(y,ys),x) -> #less#(y,x) insertD#1#(dd(y,ys),x) -> insertD#2#(#less(y,x),x,y,ys) insertD#2#(#true(),x,y,ys) -> insertD#(x,ys) insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(15) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(15) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(15) #cklt :: ["A"(0)] -(0)-> "A"(13) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(9) #false :: [] -(0)-> "A"(1) #false :: [] -(0)-> "A"(15) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(12) #neg :: ["A"(5)] -(5)-> "A"(5) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(5)] -(5)-> "A"(5) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(5)] -(5)-> "A"(5) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(1) #true :: [] -(0)-> "A"(0) #true :: [] -(0)-> "A"(15) dd :: ["A"(5) x "A"(5)] -(0)-> "A"(5) dd :: ["A"(6) x "A"(6)] -(0)-> "A"(6) dd :: ["A"(12) x "A"(12)] -(0)-> "A"(12) dd :: ["A"(8) x "A"(8)] -(0)-> "A"(8) dd :: ["A"(15) x "A"(15)] -(0)-> "A"(15) insert :: ["A"(10) x "A"(5)] -(0)-> "A"(5) insert#1 :: ["A"(5) x "A"(10)] -(0)-> "A"(5) insert#2 :: ["A"(1) x "A"(10) x "A"(5) x "A"(5)] -(0)-> "A"(5) insertD :: ["A"(8) x "A"(6)] -(0)-> "A"(6) insertD#1 :: ["A"(6) x "A"(8)] -(0)-> "A"(6) insertD#2 :: ["A"(1) x "A"(8) x "A"(6) x "A"(6)] -(0)-> "A"(6) insertionsort :: ["A"(12)] -(3)-> "A"(5) insertionsort#1 :: ["A"(12)] -(3)-> "A"(5) insertionsortD :: ["A"(8)] -(8)-> "A"(6) insertionsortD#1 :: ["A"(8)] -(8)-> "A"(6) nil :: [] -(0)-> "A"(5) nil :: [] -(0)-> "A"(6) nil :: [] -(0)-> "A"(12) nil :: [] -(0)-> "A"(8) nil :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(11) nil :: [] -(0)-> "A"(13) #compare# :: ["A"(5) x "A"(5)] -(3)-> "A"(1) #less# :: ["A"(5) x "A"(15)] -(5)-> "A"(0) insert# :: ["A"(15) x "A"(5)] -(12)-> "A"(0) insert#1# :: ["A"(5) x "A"(15)] -(12)-> "A"(0) insert#2# :: ["A"(0) x "A"(15) x "A"(1) x "A"(5)] -(12)-> "A"(0) insertD# :: ["A"(15) x "A"(5)] -(6)-> "A"(0) insertD#1# :: ["A"(5) x "A"(15)] -(6)-> "A"(0) insertD#2# :: ["A"(0) x "A"(15) x "A"(0) x "A"(5)] -(6)-> "A"(0) insertionsort# :: ["A"(15)] -(15)-> "A"(0) insertionsort#1# :: ["A"(15)] -(15)-> "A"(0) insertionsortD# :: ["A"(15)] -(15)-> "A"(0) insertionsortD#1# :: ["A"(15)] -(15)-> "A"(0) c_13 :: ["A"(0)] -(1)-> "A"(1) c_17 :: ["A"(0)] -(0)-> "A"(15) c_19 :: ["A"(0)] -(0)-> "A"(12) c_20 :: ["A"(1)] -(0)-> "A"(1) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(1)] -(1)-> "A"(1) "#pos_A" :: ["A"(1)] -(1)-> "A"(1) "#s_A" :: ["A"(1)] -(1)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_13_A" :: ["A"(0)] -(1)-> "A"(1) "c_17_A" :: ["A"(0)] -(0)-> "A"(1) "c_19_A" :: ["A"(0)] -(0)-> "A"(1) "c_20_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) 2. Weak: #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) *** Step 6.b:1.b:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) - Weak DPs: #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)) #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)) #less#(x,y) -> c_20(#compare#(x,y)) insert#(x,l) -> insert#1#(l,x) insert#1#(dd(y,ys),x) -> #less#(y,x) insert#1#(dd(y,ys),x) -> insert#2#(#less(y,x),x,y,ys) insert#2#(#true(),x,y,ys) -> insert#(x,ys) insertD#(x,l) -> insertD#1#(l,x) insertD#1#(dd(y,ys),x) -> #less#(y,x) insertD#1#(dd(y,ys),x) -> insertD#2#(#less(y,x),x,y,ys) insertD#2#(#true(),x,y,ys) -> insertD#(x,ys) insertionsort#(l) -> insertionsort#1#(l) insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort#1#(dd(x,xs)) -> insertionsort#(xs) insertionsortD#(l) -> insertionsortD#1#(l) insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)) insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) insert(x,l) -> insert#1(l,x) insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys) insert#1(nil(),x) -> dd(x,nil()) insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys)) insertD(x,l) -> insertD#1(l,x) insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys) insertD#1(nil(),x) -> dd(x,nil()) insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys)) insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys)) insertionsort(l) -> insertionsort#1(l) insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort#1(nil()) -> nil() insertionsortD(l) -> insertionsortD#1(l) insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs)) insertionsortD#1(nil()) -> nil() - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2 ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1 ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2 ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0 ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD# ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(14) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(6) #LT :: [] -(0)-> "A"(14) #cklt :: ["A"(0)] -(0)-> "A"(0) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #false :: [] -(0)-> "A"(0) #false :: [] -(0)-> "A"(8) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #neg :: ["A"(0)] -(0)-> "A"(0) #neg :: ["A"(4)] -(0)-> "A"(4) #pos :: ["A"(4)] -(4)-> "A"(4) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(4)] -(4)-> "A"(4) #true :: [] -(0)-> "A"(0) dd :: ["A"(6) x "A"(6)] -(6)-> "A"(6) dd :: ["A"(4) x "A"(4)] -(4)-> "A"(4) dd :: ["A"(14) x "A"(14)] -(14)-> "A"(14) dd :: ["A"(15) x "A"(15)] -(15)-> "A"(15) dd :: ["A"(7) x "A"(7)] -(7)-> "A"(7) dd :: ["A"(8) x "A"(8)] -(8)-> "A"(8) insert :: ["A"(13) x "A"(6)] -(8)-> "A"(6) insert#1 :: ["A"(6) x "A"(13)] -(8)-> "A"(6) insert#2 :: ["A"(0) x "A"(13) x "A"(6) x "A"(6)] -(14)-> "A"(6) insertD :: ["A"(4) x "A"(4)] -(4)-> "A"(4) insertD#1 :: ["A"(4) x "A"(4)] -(4)-> "A"(4) insertD#2 :: ["A"(0) x "A"(4) x "A"(4) x "A"(4)] -(8)-> "A"(4) insertionsort :: ["A"(14)] -(0)-> "A"(6) insertionsort#1 :: ["A"(14)] -(0)-> "A"(6) insertionsortD :: ["A"(6)] -(13)-> "A"(4) insertionsortD#1 :: ["A"(6)] -(12)-> "A"(4) nil :: [] -(0)-> "A"(6) nil :: [] -(0)-> "A"(4) nil :: [] -(0)-> "A"(14) #compare# :: ["A"(4) x "A"(4)] -(6)-> "A"(0) #less# :: ["A"(4) x "A"(4)] -(6)-> "A"(8) insert# :: ["A"(8) x "A"(4)] -(12)-> "A"(8) insert#1# :: ["A"(4) x "A"(8)] -(12)-> "A"(8) insert#2# :: ["A"(0) x "A"(8) x "A"(0) x "A"(4)] -(12)-> "A"(8) insertD# :: ["A"(4) x "A"(4)] -(4)-> "A"(8) insertD#1# :: ["A"(4) x "A"(4)] -(4)-> "A"(8) insertD#2# :: ["A"(0) x "A"(4) x "A"(0) x "A"(4)] -(4)-> "A"(8) insertionsort# :: ["A"(15)] -(15)-> "A"(6) insertionsort#1# :: ["A"(15)] -(15)-> "A"(6) insertionsortD# :: ["A"(7)] -(15)-> "A"(8) insertionsortD#1# :: ["A"(7)] -(12)-> "A"(8) c_13 :: ["A"(0)] -(0)-> "A"(14) c_17 :: ["A"(0)] -(0)-> "A"(0) c_19 :: ["A"(0)] -(0)-> "A"(0) c_20 :: ["A"(0)] -(0)-> "A"(12) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(1)] -(0)-> "A"(1) "#pos_A" :: ["A"(1)] -(1)-> "A"(1) "#s_A" :: ["A"(1)] -(1)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_13_A" :: ["A"(0)] -(0)-> "A"(1) "c_17_A" :: ["A"(0)] -(0)-> "A"(1) "c_19_A" :: ["A"(0)] -(0)-> "A"(1) "c_20_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)) 2. Weak: WORST_CASE(?,O(n^3))